The main goal of this PR is to change the implementation of the failure preservation check. If L is a left mover and X is an arbitrary action, the new formulation requires proving the validity of the following condition:

wlp(L, gate(X)) ==> gate(X)

This implication can be stated informally as either of the following two equivalent conditions.

• if it is impossible to get an execution of L from a state s leading either to a failure of L or to a state violating gate(X), then s also satisfies gate(X)
• if s fails gate(X), then there is a way to execute L from s leading either to a failure of L or to a state that fails gate(X)

A useful aspect of the new formulation is that when the check fails, blame can be assigned to a specific assertion in gate(X). This is because the right side of the implication has a separate conjunct corresponding to each assert.

It is a conjecture that if we check this new formulation of failure preservation on a left mover, then the non-blocking check on a left mover can be dropped. Intuitively, this new formulation appears to capture the essential aspects of the old formulation of failure preservation and the non-blocking check in one condition.

We would like the failure preservation check to have the desirable property that if variables accessed in L are disjoint from those accessed in gate(X), then the check is guaranteed to succeed. The proposed failure preservation check does not have this property. But by separately proving that L is nonblocking, we can reclaim this property for the proposed check. Note that the nonblocking check is logically the same as proving the validity wlp(L, false) ==> false.

Additionally:

• As a side effect of making the new formulation work on existing Civl samples, add_to_pool annotations on assertions had to be propagated in gate computation.
• To simplify gate computation, we now enforce that atomic actions cannot refer to old(.).
• A small bug in pool instantiation was fixed.
• Error messages for mover checks were improved.
• 2PC proof based on inductive sequentialization is deleted because it needed some porting and is going to be replaced anyway by an alternative proof based on the new proof rule by @NamrathaG.
• Cooperation --> Nonblocking